/* Bozza del type-checker dei tipi semplici per il Pi-calcolo poliadico */

/* Grammatica

se C e' una categoria sintattica allora C* e' una sequenza finita (eventualmente vuota) di
espressioni di categoria C (realizzata con una lista)

Var ::= a| b | c | x | y | z | Var i   (i in Nat)

Num ::= 0 | 1 | ...

Bool ::= true | false

Exp ::= Var | Num | Bool | Exp + Exp | Exp and Exp

Proc ::= stop | input(Var, Var*, Proc) | rec(Var, Var*, Proc)
      |  output(Var, Exp*, Proc) | par(Proc, Proc) | nu(Var, Proc)
      |  ite(Exp, Proc, Proc)

Type ::= int | bool | chan(Type*)    

Typing ::= hasType(Var, Type)

Env ::= Typing*

*/

% Operatori

:- op(110, xfx, and).
:- op(110, xfx, neq).

% Utilita'

member(X, [X]).
member(X, [X|_]).
member(X, [_|Y]) :- member(X,Y).

% Predicati relativi alle cat. sintattiche

is_Var(X) :-
	atom(X),
	name(X, [A | L]),
	member(A, [97, 98, 99, 120, 121, 122]), !,
	name(Y, L),
	(Y = ''; integer(Y)).

% Predicati relativi agli ambienti

inDom(Var, [hasType(Var,_)|_]).

inDom(Var, [_|Delta]) :- inDom(Var, Delta).

typeInEnv(Var, T, [hasType(Var,T)|_]).

typeInEnv(Var, T, [_|Delta]) :- typeInEnv(Var, T, Delta).

merge_Env([hasType(Var, T)|_], Delta2, _) :-
	not(member(hasType(Var, T), Delta2)),
	inDom(Var, Delta2), !, fail.

merge_Env([], Delta, Delta) :- !.

merge_Env([hasType(Var,T)|Delta1], Delta2, Delta3) :-
	member(hasType(Var,T), Delta2), !,
	merge_Env(Delta1, Delta2, Delta3).

merge_Env([hasType(Var,T)|Delta1], Delta2, [hasType(Var,T)|Delta3]) :-
	merge_Env(Delta1, Delta2, Delta3).

% Assegnamento per le espressioni

der(_, true, bool).

der(_, false, bool).

der(_, stop, proc).

/* Versione piu' complicata dell'assioma: forse inutile

der([hasType(Var,T)], Var, T) :- 
      is_Var(Var), !.

der(Delta, Var, T) :-
      is_Var(Var),
      typeInEnv(Var, T, Delta).
      
der([hasType(Var,T)|Delta], Var, T) :-
      is_Var(Var),
      not(inDom(Var,Delta)).
      
*/

der(Delta, input(Chan, Input, P), proc) :-
	der(Delta1, P, proc), !,
	merge_Env([hasType(Chan, chan(T)), hasType(Input, T)], Delta1, Delta2), !,
	delete(Delta2, hasType(Input, _), Delta).

der(Delta, rec(Chan, Input, P), proc) :-
	der(Delta1, P, proc), !,
	merge_Env([hasType(Chan, chan(T)), hasType(Input, T)], Delta1, Delta2), !,
	delete(Delta2, hasType(Input, _), Delta).

der(Delta, output(Chan, Output, P), proc) :-
	der(Delta1, P, proc),
	der(Delta2, Output, T),
	merge_Env([hasType(Chan, chan(T))], Delta1, Delta3),
	merge_Env(Delta3, Delta2, Delta), !.

der(Delta, par(P, Q), proc) :-
	der(Delta1, P, proc),
	der(Delta2, Q, proc),
	merge_Env(Delta1, Delta2, Delta).

der(Delta, nu(Chan, P), proc) :-
	der(Delta1, P, proc),
	typeInEnv(Chan,chan(_),Delta1),
	delete(Delta1, hasType(Chan,chan(_)), Delta),
	(\+inDom(Chan,Delta) ; !, fail).

der(Delta, ite(Exp, Proc1, Proc2), proc) :-
	der(Delta1, Exp, bool),
	der(Delta2, Proc1, proc),
	der(Delta3, Proc2, proc),
	merge_Env(Delta1, Delta2, DeltaT),
	merge_Env(Delta3, DeltaT, Delta), !.

der(_, Num, int) :- integer(Num).

der([hasType(Var,T)], Var, T) :-
	is_Var(Var).

der(Delta, Exp, T) :-
	Exp =.. E,
	der_E(Delta, E, T).

der_E(Delta, [F, Exp1, Exp2], int) :-
	member(F, ['+', '*', '-', '/']), !,
	der_E_M(Exp1, Exp2, int, Delta).

der_E(Delta, [F, Exp1, Exp2], bool) :-
	member(F, ['and', 'or']), !,
	der_E_M(Exp1, Exp2, bool, Delta).

der_E(Delta, [F, Exp1, Exp2], bool) :-
	member(F, ['=', 'neq', '>', '<']), !,
	der_E_M(Exp1, Exp2, _, Delta).

der_E_M(Exp1, Exp2, T, Delta) :-
	der(Delta1, Exp1, T),
	der(Delta2, Exp2, T),
	merge_Env(Delta1, Delta2, Delta).

write_Env([]).

write_Env([hasType(V, Ty)]) :-
	print_Env('.~n', [V, Ty]), !.

write_Env([hasType(V, Ty) | T]) :-
	print_Env(',~n', [V, Ty]),
	write_Env(T).

print_Env(Sep, [V, T]) :-
	(atom(T) ; gensym(t, Ty), T = Ty), !,
	string_concat('~a : ~a', Sep, STP),
	format(STP, [V, T]).

print_Env(Sep, [V, chan(T)]) :-
	(atom(T) ; gensym(t, Ty), chan(T) = chan(Ty)),
	string_concat('~a : chan(~a)', Sep, STP),
	format(STP, [V, T]).
